es:ES, e1, e2, b:E, Q, P:({e:E| loc(e) = loc(e1)  Id }{e:E| loc(e) = loc(e1)  Id }Prop).
(e1 <loc b)
 b  e2 
 [e1;pred(b)]~([a,b].P(a,b))*[a,b].P(a,b)
 [b;e2]~([a,b].P(a,b))*[a,b].Q(a,b)
 [e1;e2]~([a,b].P(a,b))*[a,b].Q(a,b) 

latex

Definitions

x:A. B(x), Prop, P  Q, [e1;e2]~([a,b].p(a;b))*[a,b].q(a;b), x(s1,s2), x:A. B(x), t  T, x,y. t(x;y), {i..j}, if b t else f fi, i  j < k, true, P  Q, P & Q, P  Q, false, T, True, SQType(T), {T}, AB, A, False, A & B, (e <loc e'), , , Unit,

Lemmas

es-pstar-q wf, es-le-loc, es-loc-pred, es-locl-iff, Id wf, es-loc wf, subtype rel self, es-E wf, es-pred wf, es-le wf, es-locl wf, event system wf, lt int wf, bool wf, iff transitivity, assert wf, eqtt to assert, assert of lt int, le wf, le int wf, bnot wf, eqff to assert, squash wf, true wf, bnot of lt int, assert of le int, Id sq, int seg wf, int seg properties, es-le-trans2, es-pred-locl, not wf, es-first wf